minus2(x, y) -> cond3(gt2(x, y), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
minus2(x, y) -> cond3(gt2(x, y), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
MINUS2(x, y) -> COND3(gt2(x, y), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
GT2(s1(u), s1(v)) -> GT2(u, v)
MINUS2(x, y) -> GT2(x, y)
minus2(x, y) -> cond3(gt2(x, y), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS2(x, y) -> COND3(gt2(x, y), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
GT2(s1(u), s1(v)) -> GT2(u, v)
MINUS2(x, y) -> GT2(x, y)
minus2(x, y) -> cond3(gt2(x, y), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
minus2(x, y) -> cond3(gt2(x, y), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
MINUS2(x, y) -> COND3(gt2(x, y), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
minus2(x, y) -> cond3(gt2(x, y), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
MINUS2(x, y) -> COND3(gt2(x, y), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
minus2(x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
MINUS2(x, y) -> COND3(gt2(x, y), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
MINUS2(0, x0) -> COND3(false, 0, x0)
MINUS2(s1(x0), s1(x1)) -> COND3(gt2(x0, x1), s1(x0), s1(x1))
MINUS2(s1(x0), 0) -> COND3(true, s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
MINUS2(0, x0) -> COND3(false, 0, x0)
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(s1(x0), s1(x1)) -> COND3(gt2(x0, x1), s1(x0), s1(x1))
MINUS2(s1(x0), 0) -> COND3(true, s1(x0), 0)
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(s1(x0), s1(x1)) -> COND3(gt2(x0, x1), s1(x0), s1(x1))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ UsableRulesProof
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
MINUS2(s1(x0), s1(x1)) -> COND3(gt2(x0, x1), s1(x0), s1(x1))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
MINUS2(s1(z0), s1(s1(z1))) -> COND3(gt2(z0, s1(z1)), s1(z0), s1(s1(z1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
MINUS2(s1(z0), s1(s1(z1))) -> COND3(gt2(z0, s1(z1)), s1(z0), s1(s1(z1)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
MINUS2(x, y) -> COND3(gt2(x, y), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
minus2(x0, x1)
gt2(s1(x0), s1(x1))
cond3(true, x0, x1)
gt2(s1(x0), 0)
cond3(false, x0, x1)
minus2(x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MINUS2(x, y) -> COND3(gt2(x, y), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)